home *** CD-ROM | disk | FTP | other *** search
/ Celestin Apprentice 4 / Apprentice-Release4.iso / Source Code / C / Applications / SML⁄NJ 93+ / Documentation / examples / powerset.sml < prev    next >
Encoding:
Text File  |  1995-12-30  |  5.5 KB  |  193 lines  |  [TEXT/R*ch]

  1. (* This is an example of the use of higher-order functors *)
  2.  
  3.  
  4. signature OrdSig =
  5.     sig
  6.     type ground
  7.     val ground_eq : ground -> ground -> bool
  8.     val ground_leq : ground -> ground -> bool
  9.     val ground_to_string : ground -> string
  10.     end
  11.  
  12.  
  13. structure NumOrd : OrdSig =
  14.     struct
  15.     type ground = int
  16.     fun ground_eq x y = (x = y)
  17.     fun ground_leq (x:int) y = x <= y
  18.     fun ground_to_string x = makestring (x:int)
  19.     end
  20.  
  21.  
  22. signature SetSig =
  23.     sig
  24.     structure Ord : OrdSig
  25.     type set
  26.     val choose : set -> Ord.ground option
  27.     val contained_in : set -> set -> bool
  28.     val empty_set : set
  29.     val insert : Ord.ground -> set -> set
  30.     val intersect : set -> set -> set
  31.     val make_set : Ord.ground list -> set
  32.     val member : Ord.ground -> set -> bool
  33.     val remove : Ord.ground -> set -> set
  34.     val set_eq : set -> set -> bool
  35.     val set_to_string : set -> string
  36.     val union : set -> set -> set
  37.     val for_every : (Ord.ground -> bool) -> set -> bool
  38.     val there_is : (Ord.ground -> bool) -> set -> bool
  39.     val allsubsets : set -> set list
  40.     end
  41.  
  42. functor SetFunc (Ord:OrdSig) : SetSig =
  43.     struct
  44.     structure Ord = Ord
  45.     local
  46.         fun mem nil a = false
  47.           | mem (hd::tl) a = if Ord.ground_eq hd a
  48.                      then true
  49.                  else mem tl a
  50.     in abstype set = set of Ord.ground list
  51.         with val empty_set = set nil
  52.         fun insert e (set es) = 
  53.             if mem es e then set es
  54.             else set (e::es)
  55.         fun choose (set []) = NONE
  56.           | choose (set (e::es)) = SOME e
  57.         fun member e (set es) = mem es e
  58.         fun union (set []) (set es) = set es
  59.           | union (set (e::es1)) (set es2) = 
  60.             insert e (union (set es1) (set es2))
  61.         fun intersect (set []) (set es) = set []
  62.           | intersect (set es) (set []) = set []
  63.           | intersect (set (e::es1)) (set es2) =
  64.             if mem es2 e then
  65.             case (intersect (set es1) (set es2)) of
  66.                 set es => set (e::es)
  67.             else intersect (set es1) (set es2)
  68.         fun remove e (set []) = set []
  69.           | remove e (set (e1::es)) = 
  70.             if Ord.ground_eq e e1 then set es
  71.             else set (e1::(case  remove e (set es) of set es1 => es1))
  72.         (* another way to write the prev. line
  73.                     else let val set es1 = remove e (set es)
  74.                           in set (e1 :: es1) end
  75.          *)
  76.         fun contained_in (set []) (set es) = true
  77.           | contained_in (set (e::es1)) (set es) =
  78.             (mem es e) andalso (contained_in (set es1) (set es))
  79.         fun set_to_string (set l) =
  80.              let fun conv (nil) = ""
  81.                |  conv (a::nil) = Ord.ground_to_string a
  82.                |  conv (a::b) =
  83.                     (Ord.ground_to_string a) ^ "," ^ conv b
  84.              in "{" ^ conv(l) ^ "}" end
  85.         fun for_every P (set []) = true
  86.           | for_every P (set (x::xs)) =
  87.              (P x) andalso (for_every P (set xs))
  88.  
  89.         fun there_is P (set []) = false
  90.           | there_is P (set (x::xs)) =
  91.              (P x) orelse (there_is P (set xs))
  92.         end
  93.     end
  94.     fun set_eq s1 s2 = (contained_in s1 s2) andalso (contained_in s2 s1)
  95.     fun make_set [] = empty_set
  96.       | make_set (hd::tl) = insert hd (make_set tl)
  97.     fun allsubsets set =
  98.         (case choose set
  99.            of NONE => [empty_set]
  100.             | SOME elt =>
  101.               let
  102.               val subsets_without_elt = allsubsets(remove elt set)
  103.               in
  104.               subsets_without_elt @
  105.               (map (insert elt) subsets_without_elt)
  106.               end)
  107.     end (* functor SetFunc *)
  108.  
  109.  
  110. functor SetContOrdFunc (Set : SetSig) : OrdSig =
  111.     struct
  112.     type ground = Set.set
  113.     val ground_eq = Set.set_eq
  114.     val ground_leq = Set.contained_in
  115.     val ground_to_string = Set.set_to_string
  116.     end
  117.  
  118.  
  119. functor SetHoareOrdFunc (Set : SetSig) : OrdSig =
  120.     struct
  121.     type ground = Set.set
  122.     val ground_to_string = Set.set_to_string
  123.     fun ground_leq smaller_set bigger_set =
  124.           Set.for_every
  125.            (fn big => (Set.there_is
  126.                (fn small => Set.Ord.ground_leq small big)
  127.                smaller_set))
  128.            bigger_set
  129.     fun ground_eq set1 set2 = ground_leq set1 set2 andalso
  130.                               ground_leq set2 set1
  131.  
  132.     end
  133.  
  134.  
  135. functor SetSmytheOrdFunc (Set : SetSig) : OrdSig =
  136.     struct
  137.     type ground = Set.set
  138.     val ground_to_string = Set.set_to_string
  139.     fun ground_leq smaller_set bigger_set =
  140.           Set.for_every
  141.            (fn small => (Set.there_is
  142.                  (fn big => Set.Ord.ground_leq small big)
  143.                 bigger_set))
  144.            smaller_set
  145.     fun ground_eq set1 set2 = ground_leq set1 set2 andalso
  146.                               ground_leq set2 set1
  147.     end
  148.  
  149. signature PowersetSig =
  150.     sig
  151.     structure Set : SetSig
  152.     structure Powerset : SetSig
  153.     sharing type Set.set = Powerset.Ord.ground
  154.     val powerset : Set.set -> Powerset.set
  155.     end
  156.  
  157. functor PowersetFunc (functor SetOrdFunc(Set : SetSig)
  158.               : sig 
  159.                 type ground
  160.                 val ground_eq : ground -> ground -> bool
  161.                 val ground_leq : ground -> ground -> bool
  162.                 val ground_to_string : ground -> string
  163.                 sharing type Set.set = ground
  164.                 end
  165.               structure Ord : OrdSig) : PowersetSig =
  166.     struct    
  167.     structure Set = SetFunc(Ord)
  168.     structure Powerset = SetFunc(SetOrdFunc(Set))
  169.     fun powerset set = Powerset.make_set (Set.allsubsets set)
  170.     end
  171.  
  172.  
  173. structure NumPowerset = PowersetFunc(functor SetOrdFunc = SetContOrdFunc
  174.                      structure Ord = NumOrd)
  175.  
  176. structure HoarePowerset = PowersetFunc(functor SetOrdFunc = SetHoareOrdFunc
  177.                        structure Ord = NumOrd)
  178.  
  179. structure SmythePowerset = PowersetFunc(functor SetOrdFunc = SetSmytheOrdFunc
  180.                     structure Ord = NumOrd);
  181.  
  182.  
  183. val ans1 = NumPowerset.Powerset.set_to_string
  184.             (NumPowerset.powerset (NumPowerset.Set.make_set [1,2,3,4]));
  185.  
  186. val ans2 = HoarePowerset.Powerset.set_to_string
  187.             (HoarePowerset.powerset (HoarePowerset.Set.make_set [1,2,3,4]));
  188.  
  189. val ans3 = SmythePowerset.Powerset.set_to_string
  190.             (SmythePowerset.powerset (SmythePowerset.Set.make_set [1,2,3,4]));
  191.  
  192.  
  193.